\begin{tabbing}
disjoint\_sublists($T$;$L_{1}$;$L_{2}$;$L$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\exists$\=$f_{1}$:\{0..$\parallel$$L_{1}$$\parallel^{-}$\}$\rightarrow$\{0..$\parallel$$L$$\parallel^{-}$\}\+
\\[0ex]$\exists$\=$f_{2}$:\{0..$\parallel$$L_{2}$$\parallel^{-}$\}$\rightarrow$\{0..$\parallel$$L$$\parallel^{-}$\}\+
\\[0ex](increasing($f_{1}$;$\parallel$$L_{1}$$\parallel$) \& ($\forall$$j$:\{0..$\parallel$$L_{1}$$\parallel^{-}$\}. $L_{1}$[$j$] = $L$[($f_{1}$($j$))])
\\[0ex]\& increasing($f_{2}$;$\parallel$$L_{2}$$\parallel$) \& ($\forall$$j$:\{0..$\parallel$$L_{2}$$\parallel^{-}$\}. $L_{2}$[$j$] = $L$[($f_{2}$($j$))])
\\[0ex]\& ($\forall$$j_{1}$:\{0..$\parallel$$L_{1}$$\parallel^{-}$\}, $j_{2}$:\{0..$\parallel$$L_{2}$$\parallel^{-}$\}. $\neg$($f_{1}$($j_{1}$) = $f_{2}$($j_{2}$))))
\-\-
\end{tabbing}